es-LnkTag-deq  EqDecider(:IdLnk  Id) 

latex

Definitions	t  T, es-LnkTag-deq, x:A. B(x)
Lemmas	product-deq wf, IdLnk wf, Id wf, idlnk-deq wf, id-deq wf